\begin{tabbing}
ma{-}sub\=\{i:l\}\+
\\[0ex]($M_{1}$; $M_{2}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=fpf{-}sub(Id; $x$.Type$_{\mbox{\scriptsize i}}$; IdDeq; 1of($M_{1}$); 1of($M_{2}$))\+
\\[0ex]\& fpf{-}sub(Knd; $x$.Type$_{\mbox{\scriptsize i}}$; KindDeq; 1of(2of($M_{1}$)); 1of(2of($M_{2}$)))
\\[0ex]\& \=fpf{-}sub(\=Id;\+\+
\\[0ex]$x$.fpf{-}cap(1of($M_{2}$);IdDeq;$x$;Void);
\\[0ex]IdDeq;
\\[0ex]1of(2of(2of($M_{1}$)));
\\[0ex]1of(2of(2of($M_{2}$))))
\-\\[0ex]\& fpf{-}sub(\=Id;\+
\\[0ex]$a$.(State(1of($M_{2}$))$\rightarrow$fpf{-}cap(1of(2of($M_{2}$));KindDeq;locl($a$);Top)$\rightarrow$Prop$_{\mbox{\scriptsize i}}$);
\\[0ex]IdDeq;
\\[0ex]1of(2of(2of(2of($M_{1}$))));
\\[0ex]1of(2of(2of(2of($M_{2}$)))))
\-\\[0ex]\& fpf{-}sub(\=(Knd$\times$Id);\+
\\[0ex]${\it kx}$.(State(1of($M_{2}$))$\rightarrow$Valtype(1of(2of($M_{2}$));1of(${\it kx}$))$\rightarrow$
\\[0ex]fpf{-}cap(1of($M_{2}$);IdDeq;2of(${\it kx}$);Void));
\\[0ex]product{-}deq(Knd;Id;KindDeq;IdDeq);
\\[0ex]1of(2of(2of(2of(2of($M_{1}$)))));
\\[0ex]1of(2of(2of(2of(2of($M_{2}$))))))
\-\\[0ex]\& fpf{-}sub(\=(Knd$\times$IdLnk);\+
\\[0ex]${\it kl}$.((\=${\it tg}$:Id\+
\\[0ex]$\times$(\=State(1of($M_{2}$))$\rightarrow$Valtype(1of(2of($M_{2}$));1of(${\it kl}$))$\rightarrow$\+
\\[0ex](fpf{-}cap(1of(2of($M_{2}$));KindDeq;rcv(2of(${\it kl}$),${\it tg}$);Void) List))) List);
\-\-\\[0ex]product{-}deq(Knd;IdLnk;KindDeq;IdLnkDeq);
\\[0ex]1of(2of(2of(2of(2of(2of($M_{1}$))))));
\\[0ex]1of(2of(2of(2of(2of(2of($M_{2}$)))))))
\-\\[0ex]\& fpf{-}sub(\=Id;\+
\\[0ex]$x$.(Knd List);
\\[0ex]IdDeq;
\\[0ex]1of(2of(2of(2of(2of(2of(2of($M_{1}$)))))));
\\[0ex]1of(2of(2of(2of(2of(2of(2of($M_{2}$))))))))
\-\\[0ex]\& fpf{-}sub(\=(IdLnk$\times$Id);\+
\\[0ex]${\it ltg}$.(Knd List);
\\[0ex]product{-}deq(IdLnk;Id;IdLnkDeq;IdDeq);
\\[0ex]1of(2of(2of(2of(2of(2of(2of(2of($M_{1}$))))))));
\\[0ex]1of(2of(2of(2of(2of(2of(2of(2of($M_{2}$)))))))))
\-\\[0ex]\& fpf{-}sub(\=Knd;\+
\\[0ex]$k$.(Id List);
\\[0ex]KindDeq;
\\[0ex]1of(2of(2of(2of(2of(2of(2of(2of(2of($M_{1}$)))))))));
\\[0ex]1of(2of(2of(2of(2of(2of(2of(2of(2of($M_{2}$))))))))))
\-\\[0ex]\& fpf{-}sub(\=Knd;\+
\\[0ex]$k$.(IdLnk List);
\\[0ex]KindDeq;
\\[0ex]1of(2of(2of(2of(2of(2of(2of(2of(2of(2of($M_{1}$))))))))));
\\[0ex]1of(2of(2of(2of(2of(2of(2of(2of(2of(2of($M_{2}$)))))))))))
\-\\[0ex]\& fpf{-}sub(\=Id;\+
\\[0ex]$x$.(Knd List);
\\[0ex]IdDeq;
\\[0ex]1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of($M_{1}$)))))))))));
\\[0ex]1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of($M_{2}$))))))))))))
\-\-\-
\end{tabbing}